$\forall$$T$:Type, ${\it dT}$:EqDecider($T$), $L$:($T$ List). ($\neg$($\uparrow$null($L$))) $\Rightarrow$ (index($L$;hd($L$)) $\sim$ 0)